LISPAX.PRF[W82,JMC]2 - www.SailDart.org

perm filename LISPAX.PRF[W82,JMC]2 blob sn#656469 filedate 1982-05-03 generic text, type T, neo UTF8
;;; DEFINFO containing recursive function definitions,
;;; SIMPINFO used for simplifying, and
;;; SORTINFO used for determining the sorts expressions for lambda conversion.
;;; etc.

(proof lispax)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(decl (xa ya za) |ground| variable atom)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (~) |GROUND⊗GROUND→GROUND| CONsTANT NIL (INFIX 850))

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT nil (unary 950))

(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONsTANT nil (unary 750))

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT nil (unary 750))

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT nil (unary 750))

(AXIOM |∀U.sEXP U |)
(lname sortinfo)

(AXIOM |∀X U.LISTP X~U |)
(lname sortinfo simpinfo)

(AXIOM |∀U.NULL U ≡ U=NNIL|)
(lname nilprop)
(axiom |atom nnil|)
(lname nilprop)
(axiom |∀u.atom u ⊃ u=nnil|)
(lname nilprop)

(axiom |null nnil|)
(lname simpinfo nilprop)

(AXIOM |∀X Y.SEXP X~Y|)
(lname sortinfo)

(AXIOM |∀X Y.¬ATOM X~Y|)
(lname consfacts simpinfo)

(AXIOM |∀X U.¬NULL X~U|)
(lname consfacts simpinfo)

(AXIOM |∀X U.CAR (X ~ U) = X|)
(lname simpinfo)

(AXIOM |∀X U.CDR (X~U) = U|)
(lname simpinfo)

(AXIOM |∀X Y.CAR (X ~ Y) = X|)
(lname consfacts simpinfo)

(AXIOM |∀X Y.CDR (X~Y) = Y|)
(lname consfacts simpinfo)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
(lname listinduction)

(AXIOM |∀PHI.(∀X.ATOM X ⊃ PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
(lname sexpinduction)

;;; Lists of variable numbers of arguments require special treatment.

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)
(lname sortinfo)

(axiom |∀x.list(x) = x~nnil|)
(lname simpinfo)

(axiom |∀x y.listp(list(x,y))|)
(lname sortinfo)

(axiom |∀x y.list(x,y) = x~list(y)|)
(lname simpinfo)

(axiom |∀x y z.listp(list(x,y,z))|)
(lname sortinfo)

(axiom |∀x y z.list(x,y,z) = x~list(y,z)|)
(lname simpinfo)

;;; some defined functions and theorems taken as axioms


(DECL (*) |GROUND⊗ground*→GROUND| functional NIL INFIX 840 both)
;;; This is LISP's append.  While it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.

(axiom |∀u v.listp(u*v)|)
(lname sortinfo listappend)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CAR U ~ (CDR U *V)|)
(lname definfo)

(axiom |∀u.nnil*u=u|)
(lname appendfacts simpinfo)

(axiom |∀x u v.x~u*v = x~(u*v)|)
(lname appendfacts simpinfo)

;;; (axiom |∀u v w.(u*v)*w = u*(v*w)|)
;;; (lname assocappend)
;;; not needed any more

(decl (alist a0 a1 a2) ground variable alistp)
(axiom |∀alist. listp alist|)
(lname simpinfo sortinfo)
(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp ((xa ~ y) ~ alist)|)
(lname mkalist)

(decl assoc |ground⊗ground → ground| constant)

(axiom |∀x alist. assoc(x,alist) =
                       if null alist then nnil
                       else if x = car car alist then car alist
                       else assoc(x, cdr alist)|)
(lname definfo)

(axiom |∀x alist.sexp assoc(x,alist)|)
(lname sortinfo)

(decl member |ground⊗ground → truthval| constant)

(axiom |∀x u. member(x,u) ≡ ¬null u ∧ (x = car u ∨ member(x, cdr u))|)
(lname definfo)

(decl (reverse) |ground→ground| constant nil unary 950)

(axiom |∀u.listp(reverse(u))|)
(lname sortinfo)

(axiom |∀u.reverse(u) = if null(u) then nnil
                        else reverse(cdr u) * list(car u)|)
(lname definfo)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(lname reverseappend)

(axiom |∀u.reverse(reverse(u)) = u|)
(lname reversereverse)

(decl subst |ground⊗ground⊗ground → ground| constant)
(axiom |∀x y z.subst(x,y,z) = if atom z then (if z = y then x else z)
                              else subst(x,y,car z)~subst(x,y,cdr z)|)
(lname definfo)
(VERS1 0 (NIL ((LINENAME REVERSEREVERSE (LN& #& . 0)) (LINENAME REVERSEAPPEND (LN& #& . 22)) (LINENAME MKALIST (LN& #& . 26)) (LINENAME APPENDFACTS (LN& #& . 49) (LN& #& . 52)) (LINENAME DEFINFO (LN& #& . 53) (LN& #& . 64) (LN& #& . 67) (LN& #& . 70) (LN& #& . 74)) (LINENAME LISTAPPEND (LN& #& . 77)) (LINENAME SEXPINDUCTION (LN& #& . 81)) (LINENAME LISTINDUCTION (LN& #& . 84)) (LINENAME CONSFACTS (LN& #& . 85) (LN& #& . 86) (LN& #& . 87) (LN& #& . 88)) (LINENAME NILPROP (LN& #& . 89) (LN& #& . 90) (LN& #& . 91) (LN& #& . 92)) (LINENAME SIMPINFO (LN& #& . 93) (LN& #& . 92) (LN& #& . 85) (LN& #& . 86) (LN& #& . 94) (LN& #& . 95) (LN& #& . 87) (LN& #& . 88) (LN& #& . 96) (LN& #& . 97) (LN& #& . 98) (LN& #& . 49) (LN& #& . 52) (LN& #& . 99)) (LINENAME SORTINFO (LN& #& . 100) (LN& #& . 93) (LN& #& . 104) (LN& #& . 105) (LN& #& . 106) (LN& #& . 107) (LN& #& . 77) (LN& #& . 99) (LN& #& . 108) (LN& #& . 109))) (LISPAX (#& . 5) (#& . 35) (#& . 41) (#& . 110) (#& . 83) (#& . 51) (#& . 114) (#& . 47) (#& . 55) (#& . 60) (#& . 79) (#& . 102) (#& . 100) (#& . 116) (#& . 93) (#& . 117) (#& . 89) (#& . 118) (#& . 90) (#& . 119) (#& . 91) (#& . 120) (#& . 92) (#& . 121) (#& . 104) (#& . 122) (#& . 85) (#& . 123) (#& . 86) (#& . 124) (#& . 94) (#& . 125) (#& . 95) (#& . 126) (#& . 87) (#& . 127) (#& . 88) (#& . 128) (#& . 84) (#& . 129) (#& . 81) (#& . 130) (#& . 72) (#& . 105) (#& . 131) (#& . 96) (#& . 132) (#& . 106) (#& . 133) (#& . 97) (#& . 134) (#& . 107) (#& . 135) (#& . 98) (#& . 136) (#& . 24) (#& . 77) (#& . 137) (#& . 53) (#& . 138) (#& . 49) (#& . 139) (#& . 52) (#& . 140) (#& . 28) (#& . 99) (#& . 141) (#& . 142) (#& . 26) (#& . 143) (#& . 66) (#& . 64) (#& . 144) (#& . 108) (#& . 145) (#& . 69) (#& . 67) (#& . 146) (#& . 2) (#& . 109) (#& . 147) (#& . 70) (#& . 148) (#& . 22) (#& . 149) (#& . 0) (#& . 150) (#& . 76) (#& . 74) (#& . 151))) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 90 .) (NIL . (COMMENTL LNAME REVERSEREVERSE) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 87 .) (NIL . (COMMENTL LNAME REVERSEAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 85 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 83 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 81 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 78 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 75 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 73 .) (NIL . (COMMENTL LNAME MKALIST) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 70 .) ((((∀ ALIST)) (⊃ (¬ (NULL ALIST)) (∧ (¬ (ATOM (CAR ALIST))) (ATOM (CAR (CAR ALIST)))))) . (AXIOM (TM& ((∀ ALIST)) (⊃ (¬ (NULL ALIST)) (∧ (¬ (ATOM (CAR ALIST))) (ATOM (CAR (CAR ALIST))))))) . NIL . ((ALIST #& . 31) (CAR #& . 54) (ATOM #& . 61) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 68 .) (NIL . (COMMENTL LNAME SIMPINFO SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 67 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 64 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 62 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 60 .) (NIL . (COMMENTL LNAME SORTINFO LISTAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 58 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 55 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 53 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 51 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 49 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 47 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 45 .) (NIL . (COMMENTL LNAME SEXPINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 42 .) (NIL . (COMMENTL LNAME LISTINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 40 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 38 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 36 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 34 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 32 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 30 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 28 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 26 .) (NIL . (COMMENTL LNAME SIMPINFO NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 24 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 22 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 20 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 18 .) (NIL . (COMMENTL LNAME SORTINFO SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 16 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 14 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 114) . CONS .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS #& . 115)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 7 .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 110) . B .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 110) . A .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 110) . C .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C #& . 111) (A #& . 112) (B #& . 113)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 4 .) ((((∀ U)) (LISTP (REVERSE U))) . (AXIOM (TM& ((∀ U)) (LISTP (REVERSE U)))) . NIL . ((U #& . 4) (LISTP #& . 78) (REVERSE #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 80 .) ((((∀ X ALIST)) (SEXP (ASSOC X ALIST))) . (AXIOM (TM& ((∀ X ALIST)) (SEXP (ASSOC X ALIST)))) . NIL . ((ASSOC #& . 65) (ALIST #& . 31) (X #& . 37) (SEXP #& . 101)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 74 .) ((((∀ X Y Z)) (LISTP (LIST X Y Z))) . (AXIOM (TM& ((∀ X Y Z)) (LISTP (LIST X Y Z)))) . NIL . ((LISTP #& . 78) (Z #& . 36) (X #& . 37) (Y #& . 34)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 52 .) ((((∀ X Y)) (LISTP (LIST X Y))) . (AXIOM (TM& ((∀ X Y)) (LISTP (LIST X Y)))) . NIL . ((LISTP #& . 78) (X #& . 37) (Y #& . 34)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 48 .) ((((∀ X)) (LISTP (LIST X))) . (AXIOM (TM& ((∀ X)) (LISTP (LIST X)))) . NIL . ((LISTP #& . 78) (X #& . 37)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 44 .) ((((∀ X Y)) (SEXP (~ X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (~ X Y)))) . NIL . ((Y #& . 34) (X #& . 37) (~ #& . 46) (SEXP #& . 101)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 25 .) (5 . |SEXP | . UNARY . 750 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((SEXP #& . 101)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 12 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 103) . (#& . 102) . SEXP .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U #& . 4) (SEXP #& . 101)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 13 .) ((((∀ ALIST)) (LISTP ALIST)) . (AXIOM (TM& ((∀ ALIST)) (LISTP ALIST))) . NIL . ((LISTP #& . 78) (ALIST #& . 31)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 66 .) ((((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z)))) . (AXIOM (TM& ((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z))))) . NIL . ((Y #& . 34) (X #& . 37) (Z #& . 36) (~ #& . 46)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 54 .) ((((∀ X Y)) (= (LIST X Y) (~ X (LIST Y)))) . (AXIOM (TM& ((∀ X Y)) (= (LIST X Y) (~ X (LIST Y))))) . NIL . ((Y #& . 34) (X #& . 37) (~ #& . 46)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 50 .) ((((∀ X)) (= (LIST X) (~ X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST X) (~ X NNIL)))) . NIL . ((X #& . 37) (NNIL #& . 50) (~ #& . 46)) . ((LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 46 .) ((((∀ X U)) (= (CDR (~ X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (~ X U)) U))) . NIL . ((U #& . 4) (X #& . 37) (~ #& . 46) (CDR #& . 56)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 33 .) ((((∀ X U)) (= (CAR (~ X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (~ X U)) X))) . NIL . ((CAR #& . 54) (~ #& . 46) (X #& . 37) (U #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 31 .) ((((∀ X U)) (LISTP (~ X U))) . (AXIOM (TM& ((∀ X U)) (LISTP (~ X U)))) . NIL . ((LISTP #& . 78) (~ #& . 46) (X #& . 37) (U #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 15 .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NULL #& . 59) (NNIL #& . 50)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 23 .) ((((∀ U)) (⊃ (ATOM U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (⊃ (ATOM U) (= U NNIL)))) . NIL . ((U #& . 4) (NNIL #& . 50) (ATOM #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 21 .) ((ATOM NNIL) . (AXIOM (TM& ATOM NNIL)) . NIL . ((ATOM #& . 61) (NNIL #& . 50)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 19 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U #& . 4) (NNIL #& . 50) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 17 .) ((((∀ X Y)) (= (CDR (~ X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (~ X Y)) Y))) . NIL . ((Y #& . 34) (X #& . 37) (~ #& . 46) (CDR #& . 56)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 37 .) ((((∀ X Y)) (= (CAR (~ X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (~ X Y)) X))) . NIL . ((CAR #& . 54) (~ #& . 46) (X #& . 37) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 35 .) ((((∀ X U)) (¬ (NULL (~ X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (~ X U))))) . NIL . ((U #& . 4) (X #& . 37) (~ #& . 46) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 29 .) ((((∀ X Y)) (¬ (ATOM (~ X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (~ X Y))))) . NIL . ((ATOM #& . 61) (~ #& . 46) (X #& . 37) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 27 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U))))) . NIL . ((~ #& . 46) (NNIL #& . 50) (PHI #& . 82) (X #& . 37) (U #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 39 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI #& . 82)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 5 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 83) . PHI .) ((((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X))))) . NIL . ((Y #& . 34) (X #& . 37) (PHI #& . 82) (~ #& . 46) (ATOM #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 41 .) (6 . |LISTP | . UNARY . 750 .) (NIL . (DECL (LISTP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((LISTP #& . 78)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 11 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 80) . (#& . 79) . LISTP .) ((((∀ U V)) (LISTP (* U V))) . (AXIOM (TM& ((∀ U V)) (LISTP (* U V)))) . NIL . ((LISTP #& . 78) (U #& . 4) (V #& . 17)) . ((* #& . 23)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 57 .) (NIL . (DECL (SUBST) (OT& (GROUND GROUND GROUND) . GROUND) CONSTANT) . NIL . ((SUBST #& . 75)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 88 .) (CONSTANT . ((GROUND GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 76) . SUBST .) ((((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))) . (AXIOM (TM& ((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))) . NIL . ((Y #& . 34) (X #& . 37) (Z #& . 36) (~ #& . 46) (CAR #& . 54) (CDR #& . 56) (ATOM #& . 61) (SUBST #& . 75)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 89 .) (4 . LIST . PREFIX . 1000 .) (NIL . (DECL (LIST) (FT& ((GROUND) GROUND NIL . GROUND)) FUNCTIONAL) . NIL . NIL . ((LIST #& . 71)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 43 .) (FUNCTIONAL . (((GROUND) GROUND NIL . GROUND)) . UNIVERSAL . NIL . (#& . 73) . (#& . 72) . LIST .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U)))))) . (AXIOM (TM& ((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U))))))) . NIL . ((REVERSE #& . 1) (NULL #& . 59) (CDR #& . 56) (CAR #& . 54) (NNIL #& . 50) (U #& . 4)) . ((* #& . 23) (LIST #& . 71)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 82 .) (NIL . (DECL (MEMBER) (OT& (GROUND GROUND) . TRUTHVAL) CONSTANT) . NIL . ((MEMBER #& . 68)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 76 .) (CONSTANT . ((GROUND GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 69) . MEMBER .) ((((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U))))))) . NIL . ((NULL #& . 59) (CDR #& . 56) (CAR #& . 54) (X #& . 37) (U #& . 4) (MEMBER #& . 68)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 77 .) (NIL . (DECL (ASSOC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((ASSOC #& . 65)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 71 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 66) . ASSOC .) ((((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST)))))) . (AXIOM (TM& ((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST))))))) . NIL . ((NULL #& . 59) (CDR #& . 56) (CAR #& . 54) (NNIL #& . 50) (X #& . 37) (ALIST #& . 31) (ASSOC #& . 65)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 72 .) (5 . |NULL | . UNARY . 750 .) (5 . |ATOM | . UNARY . 750 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 62) . (#& . 60) . ATOM .) (NIL . (DECL (ATOM NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((NULL #& . 59) (ATOM #& . 61)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 10 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 63) . (#& . 60) . NULL .) (4 . |CAR | . UNARY . 950 .) (4 . |CDR | . UNARY . 950 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 57) . (#& . 55) . CDR .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((CDR #& . 56) (CAR #& . 54)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 9 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 58) . (#& . 55) . CAR .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V)))))) . NIL . ((V #& . 17) (U #& . 4) (~ #& . 46) (CAR #& . 54) (CDR #& . 56) (NULL #& . 59)) . ((* #& . 23)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 59 .) ((((∀ X U V)) (= (* (~ X U) V) (~ X (* U V)))) . (AXIOM (TM& ((∀ X U V)) (= (* (~ X U) V) (~ X (* U V))))) . NIL . ((V #& . 17) (U #& . 4) (X #& . 37) (~ #& . 46)) . ((* #& . 23)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 63 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LISTP) . NIL . ((NNIL #& . 50) (LISTP #& . 13)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 6 .) (CONSTANT . GROUND . LISTP . NIL . NIL . (#& . 51) . NNIL .) ((((∀ U)) (= (* NNIL U) U)) . (AXIOM (TM& ((∀ U)) (= (* NNIL U) U))) . NIL . ((NNIL #& . 50) (U #& . 4)) . ((* #& . 23)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 61 .) (1 . ~ . INFIX . 850 .) (NIL . (DECL (~) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 850) . NIL . ((~ #& . 46)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 8 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 48) . (#& . 47) . ~ .) (VARIABLE . GROUND . ATOM . NIL . NIL . (#& . 41) . YA .) (4 . ATOM . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 44) . (#& . 41) . ATOM .) (VARIABLE . GROUND . ATOM . NIL . NIL . (#& . 41) . ZA .) (NIL . (DECL (XA YA ZA) (OT& . GROUND) VARIABLE ATOM) . NIL . ((ZA #& . 42) (XA #& . 40) (ATOM #& . 43) (YA #& . 45)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 3 .) (VARIABLE . GROUND . ATOM . NIL . NIL . (#& . 41) . XA .) (4 . SEXP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 39) . (#& . 35) . SEXP .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 35) . X .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 35) . Z .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z #& . 36) (X #& . 37) (SEXP #& . 38) (Y #& . 34)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 2 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 35) . Y .) (6 . ALISTP . PREFIX . 1000 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 28) . A1 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 28) . ALIST .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 28) . A0 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 28) . A2 .) (NIL . (DECL (ALIST A0 A1 A2) (OT& . GROUND) VARIABLE ALISTP) . NIL . ((A2 #& . 29) (A0 #& . 30) (ALISTP #& . 27) (ALIST #& . 31) (A1 #& . 32)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 65 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 33) . (#& . 28) . ALISTP .) ((((∀ XA Y ALIST)) (ALISTP (~ (~ XA Y) ALIST))) . (AXIOM (TM& ((∀ XA Y ALIST)) (ALISTP (~ (~ XA Y) ALIST)))) . NIL . ((ALISTP #& . 27) (ALIST #& . 31) (Y #& . 34) (XA #& . 40) (~ #& . 46)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 69 .) (1 . * . INFIX . 840 .) (NIL . (DECL (*) (FT& ((GROUND GROUND) GROUND NIL . GROUND)) FUNCTIONAL NIL INFIX 840 BOTH) . NIL . NIL . ((* #& . 23)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 56 .) (FUNCTIONAL . (((GROUND GROUND) GROUND NIL . GROUND)) . UNIVERSAL . BOTH . (#& . 25) . (#& . 24) . * .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((V #& . 17) (U #& . 4) (REVERSE #& . 1)) . ((* #& . 23)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 84 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . W2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . W0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . V3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . V1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . V .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . U2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . U0 .) (5 . LISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 14) . (#& . 5) . LISTP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . U1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . U3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . V0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . V2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . W .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . W1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . W3 .) (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) (OT& . GROUND) VARIABLE LISTP) . NIL . ((W3 #& . 6) (W1 #& . 7) (W #& . 8) (V2 #& . 9) (V0 #& . 10) (U3 #& . 11) (U1 #& . 12) (U #& . 4) (LISTP #& . 13) (U0 #& . 15) (U2 #& . 16) (V #& . 17) (V1 #& . 18) (V3 #& . 19) (W0 #& . 20) (W2 #& . 21)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 5) . U .) (8 . |REVERSE | . UNARY . 950 .) (NIL . (DECL (REVERSE) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((REVERSE #& . 1)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 79 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 3) . (#& . 2) . REVERSE .) ((((∀ U)) (= (REVERSE (REVERSE U)) U)) . (AXIOM (TM& ((∀ U)) (= (REVERSE (REVERSE U)) U))) . NIL . ((REVERSE #& . 1) (U #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 86 .))